0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 89 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 2 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇒, 0 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
selectA_in_gga(T6, .(T6, T7), T7) → selectA_out_gga(T6, .(T6, T7), T7)
selectA_in_gga(T23, .(T23, .(T23, T24)), .(T23, T24)) → selectA_out_gga(T23, .(T23, .(T23, T24)), .(T23, T24))
selectA_in_gga(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37))) → U1_gga(T33, T34, T35, T37, selectA_in_gga(T33, T35, T37))
selectA_in_gga(T59, .(T47, .(T59, T60)), .(T47, T60)) → selectA_out_gga(T59, .(T47, .(T59, T60)), .(T47, T60))
selectA_in_gga(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73))) → U2_gga(T69, T47, T70, T71, T73, selectA_in_gga(T69, T71, T73))
U2_gga(T69, T47, T70, T71, T73, selectA_out_gga(T69, T71, T73)) → selectA_out_gga(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73)))
U1_gga(T33, T34, T35, T37, selectA_out_gga(T33, T35, T37)) → selectA_out_gga(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37)))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
selectA_in_gga(T6, .(T6, T7), T7) → selectA_out_gga(T6, .(T6, T7), T7)
selectA_in_gga(T23, .(T23, .(T23, T24)), .(T23, T24)) → selectA_out_gga(T23, .(T23, .(T23, T24)), .(T23, T24))
selectA_in_gga(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37))) → U1_gga(T33, T34, T35, T37, selectA_in_gga(T33, T35, T37))
selectA_in_gga(T59, .(T47, .(T59, T60)), .(T47, T60)) → selectA_out_gga(T59, .(T47, .(T59, T60)), .(T47, T60))
selectA_in_gga(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73))) → U2_gga(T69, T47, T70, T71, T73, selectA_in_gga(T69, T71, T73))
U2_gga(T69, T47, T70, T71, T73, selectA_out_gga(T69, T71, T73)) → selectA_out_gga(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73)))
U1_gga(T33, T34, T35, T37, selectA_out_gga(T33, T35, T37)) → selectA_out_gga(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37)))
SELECTA_IN_GGA(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37))) → U1_GGA(T33, T34, T35, T37, selectA_in_gga(T33, T35, T37))
SELECTA_IN_GGA(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37))) → SELECTA_IN_GGA(T33, T35, T37)
SELECTA_IN_GGA(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73))) → U2_GGA(T69, T47, T70, T71, T73, selectA_in_gga(T69, T71, T73))
SELECTA_IN_GGA(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73))) → SELECTA_IN_GGA(T69, T71, T73)
selectA_in_gga(T6, .(T6, T7), T7) → selectA_out_gga(T6, .(T6, T7), T7)
selectA_in_gga(T23, .(T23, .(T23, T24)), .(T23, T24)) → selectA_out_gga(T23, .(T23, .(T23, T24)), .(T23, T24))
selectA_in_gga(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37))) → U1_gga(T33, T34, T35, T37, selectA_in_gga(T33, T35, T37))
selectA_in_gga(T59, .(T47, .(T59, T60)), .(T47, T60)) → selectA_out_gga(T59, .(T47, .(T59, T60)), .(T47, T60))
selectA_in_gga(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73))) → U2_gga(T69, T47, T70, T71, T73, selectA_in_gga(T69, T71, T73))
U2_gga(T69, T47, T70, T71, T73, selectA_out_gga(T69, T71, T73)) → selectA_out_gga(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73)))
U1_gga(T33, T34, T35, T37, selectA_out_gga(T33, T35, T37)) → selectA_out_gga(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37)))
SELECTA_IN_GGA(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37))) → U1_GGA(T33, T34, T35, T37, selectA_in_gga(T33, T35, T37))
SELECTA_IN_GGA(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37))) → SELECTA_IN_GGA(T33, T35, T37)
SELECTA_IN_GGA(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73))) → U2_GGA(T69, T47, T70, T71, T73, selectA_in_gga(T69, T71, T73))
SELECTA_IN_GGA(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73))) → SELECTA_IN_GGA(T69, T71, T73)
selectA_in_gga(T6, .(T6, T7), T7) → selectA_out_gga(T6, .(T6, T7), T7)
selectA_in_gga(T23, .(T23, .(T23, T24)), .(T23, T24)) → selectA_out_gga(T23, .(T23, .(T23, T24)), .(T23, T24))
selectA_in_gga(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37))) → U1_gga(T33, T34, T35, T37, selectA_in_gga(T33, T35, T37))
selectA_in_gga(T59, .(T47, .(T59, T60)), .(T47, T60)) → selectA_out_gga(T59, .(T47, .(T59, T60)), .(T47, T60))
selectA_in_gga(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73))) → U2_gga(T69, T47, T70, T71, T73, selectA_in_gga(T69, T71, T73))
U2_gga(T69, T47, T70, T71, T73, selectA_out_gga(T69, T71, T73)) → selectA_out_gga(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73)))
U1_gga(T33, T34, T35, T37, selectA_out_gga(T33, T35, T37)) → selectA_out_gga(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37)))
SELECTA_IN_GGA(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73))) → SELECTA_IN_GGA(T69, T71, T73)
SELECTA_IN_GGA(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37))) → SELECTA_IN_GGA(T33, T35, T37)
selectA_in_gga(T6, .(T6, T7), T7) → selectA_out_gga(T6, .(T6, T7), T7)
selectA_in_gga(T23, .(T23, .(T23, T24)), .(T23, T24)) → selectA_out_gga(T23, .(T23, .(T23, T24)), .(T23, T24))
selectA_in_gga(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37))) → U1_gga(T33, T34, T35, T37, selectA_in_gga(T33, T35, T37))
selectA_in_gga(T59, .(T47, .(T59, T60)), .(T47, T60)) → selectA_out_gga(T59, .(T47, .(T59, T60)), .(T47, T60))
selectA_in_gga(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73))) → U2_gga(T69, T47, T70, T71, T73, selectA_in_gga(T69, T71, T73))
U2_gga(T69, T47, T70, T71, T73, selectA_out_gga(T69, T71, T73)) → selectA_out_gga(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73)))
U1_gga(T33, T34, T35, T37, selectA_out_gga(T33, T35, T37)) → selectA_out_gga(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37)))
SELECTA_IN_GGA(T69, .(T47, .(T70, T71)), .(T47, .(T70, T73))) → SELECTA_IN_GGA(T69, T71, T73)
SELECTA_IN_GGA(T33, .(T33, .(T34, T35)), .(T33, .(T34, T37))) → SELECTA_IN_GGA(T33, T35, T37)
SELECTA_IN_GGA(T69, .(T47, .(T70, T71))) → SELECTA_IN_GGA(T69, T71)
SELECTA_IN_GGA(T33, .(T33, .(T34, T35))) → SELECTA_IN_GGA(T33, T35)
From the DPs we obtained the following set of size-change graphs: